$\forall$$A$, $B$:Type, $b$:($A$ + $B$), $f$, $L_{1}$, $L_{2}$:Top.
\\[0ex]map($f$;case $b$ of inl($a$) =$>$ $L_{1}$($a$) $\mid$ inr($a$) =$>$ $L_{2}$($a$))
\\[0ex]$\sim$
\\[0ex]case $b$ of inl($a$) =$>$ map($f$;$L_{1}$($a$)) $\mid$ inr($a$) =$>$ map($f$;$L_{2}$($a$))